package edu.gatech.cc.concolic;

import java.io.FileWriter;
import java.io.IOException;
import java.io.OutputStreamWriter;
import java.io.PrintWriter;
import java.io.Writer;
import java.util.Collection;
import java.util.List;

import edu.gatech.cc.concolic.constraint.AND;
import edu.gatech.cc.concolic.constraint.Constraint;
import edu.gatech.cc.concolic.constraint.ConstraintVisitor;
import edu.gatech.cc.concolic.constraint.EQ;
import edu.gatech.cc.concolic.constraint.GE;
import edu.gatech.cc.concolic.constraint.GT;
import edu.gatech.cc.concolic.constraint.LE;
import edu.gatech.cc.concolic.constraint.LT;
import edu.gatech.cc.concolic.constraint.NE;
import edu.gatech.cc.concolic.constraint.NOT;
import edu.gatech.cc.concolic.constraint.OR;
import edu.gatech.cc.concolic.expression.I2B;
import edu.gatech.cc.concolic.expression.I2C;
import edu.gatech.cc.concolic.expression.I2L;
import edu.gatech.cc.concolic.expression.IADD;
import edu.gatech.cc.concolic.expression.IAND;
import edu.gatech.cc.concolic.expression.IDIV;
import edu.gatech.cc.concolic.expression.IINC;
import edu.gatech.cc.concolic.expression.IMUL;
import edu.gatech.cc.concolic.expression.INEG;
import edu.gatech.cc.concolic.expression.IOR;
import edu.gatech.cc.concolic.expression.IREM;
import edu.gatech.cc.concolic.expression.ISHL;
import edu.gatech.cc.concolic.expression.ISHR;
import edu.gatech.cc.concolic.expression.ISUB;
import edu.gatech.cc.concolic.expression.IUSHR;
import edu.gatech.cc.concolic.expression.IXOR;
import edu.gatech.cc.concolic.expression.IntegerConstant;
import edu.gatech.cc.concolic.expression.IntegerVariable;
import edu.gatech.cc.concolic.expression.L2I;
import edu.gatech.cc.concolic.expression.LADD;
import edu.gatech.cc.concolic.expression.LAND;
import edu.gatech.cc.concolic.expression.LCMP;
import edu.gatech.cc.concolic.expression.LDIV;
import edu.gatech.cc.concolic.expression.LMUL;
import edu.gatech.cc.concolic.expression.LNEG;
import edu.gatech.cc.concolic.expression.LOR;
import edu.gatech.cc.concolic.expression.LREM;
import edu.gatech.cc.concolic.expression.LSHL;
import edu.gatech.cc.concolic.expression.LSHR;
import edu.gatech.cc.concolic.expression.LSUB;
import edu.gatech.cc.concolic.expression.LUSHR;
import edu.gatech.cc.concolic.expression.LXOR;
import edu.gatech.cc.concolic.expression.LongConstant;
import edu.gatech.cc.concolic.expression.LongVariable;
import edu.gatech.cc.concolic.expression.SymbolicExpressionVisitor;
import edu.gatech.cc.concolic.expression.SymbolicVariable;
import gov.nasa.jpf.Config;

public class YicesBitVectorGenerator implements ProblemGenerator, SymbolicExpressionVisitor, ConstraintVisitor {
	
	private PrintWriter out;
	
	public YicesBitVectorGenerator(Config config) {
		this(config.getString(CONFIG_OUTFILE));
	}

	public YicesBitVectorGenerator(String filename) {

		Writer w = null;
		if (null != filename) {
			try {
				w = new FileWriter(filename);
			}
			catch (IOException e) {
			}
		}

		if (null == w) {
			w = new OutputStreamWriter(System.out);
		}

		out = new PrintWriter(w);
	}
	
	public void addConstraint(Constraint constraint) {
		addConstraint(constraint, "<unknown>");
	}
		
	public void addConstraint(Constraint constraint, String location) {
		out.print("(assert ");
		constraint.accept(this);
		out.println("); " + location);
	}

	public void addConstraints(List<Constraint> constraints) {
		for (Constraint c : constraints) {
			addConstraint(c);
		}
	}

	public void addConstraints(Constraint... constraints) {
		for (Constraint c : constraints) {
			addConstraint(c);
		}
	}

	public void addVariable(SymbolicVariable variable) {
		out.print("(define ");
		out.print(variable.name());
		out.print("::(bitvector ");

		if (variable instanceof IntegerVariable) {
			out.printf("32");
		}
		else if (variable instanceof LongVariable) {
			out.print("64");
		}
		else {
			throw new RuntimeException("Unhandled SymbolicVariable Type");
		}
		out.println("))");
	}

	public void addVariables(Collection<SymbolicVariable> variables) {
		for (SymbolicVariable v : variables) {
			addVariable(v);
		}
	}

	public void addVariables(SymbolicVariable... variables) {
		for (SymbolicVariable v : variables) {
			addVariable(v);
		}
	}

	public void close() {
		out.println("(max-sat)");
		out.close();
	}

	public void visit(LongConstant constant) {
		long l = constant.value().longValue();

		if (l < 0) {
			out.print(String.format("0b%64s", Long.toBinaryString(l)).replace(' ', '0'));
		}
		else {
			out.printf("(mk-bv 64 %d)", l);
		}
	}

	public void visit(LongVariable variable) {
		out.print(variable.name());
	}

	public void visit(IntegerConstant constant) {
		int i = constant.value().intValue();

		if (i < 0) {
			out.print(String.format("0b%32s", Integer.toBinaryString(i)).replace(' ', '0'));
		}
		else {
			out.printf("(mk-bv 32 %d)", i);
		}
	}

	public void visit(IntegerVariable variable) {
		out.print(variable.name());
	}

	public void visit(IADD add) {
		out.print("(bv-add ");
		add.left().accept(this);
		out.print(" ");
		add.right().accept(this);
		out.print(")");
	}

	public void visit(ISUB sub) {
		out.print("(bv-sub ");
		sub.left().accept(this);
		out.print(" ");
		sub.right().accept(this);
		out.print(")");
	}

	public void visit(IMUL mul) {
		out.print("(bv-mul ");
		mul.left().accept(this);
		out.print(" ");
		mul.right().accept(this);
		out.print(")");
	}

	public void visit(IDIV div) {
		out.print("(bv-add ");
		div.left().accept(this);
		out.print(" ");
		div.right().accept(this);
		out.print(")");
	}

	public void visit(IINC iinc) {
		out.print("(bv-add ");
		iinc.expression().accept(this);
		out.print(" ");
		out.print(iinc.increment());
		out.print(")");
	}

	public void visit(IREM rem) {
		out.print("(bv-urem ");
		rem.left().accept(this);
		out.print(" ");
		rem.right().accept(this);
		out.print(")");
	}

	public void visit(IAND and) {
		out.print("(bv-and ");
		and.left().accept(this);
		out.print(" ");
		and.right().accept(this);
		out.print(")");
	}

	public void visit(IOR or) {
		out.print("(bv-ior ");
		or.left().accept(this);
		out.print(" ");
		or.right().accept(this);
		out.print(")");
	}

	public void visit(IXOR xor) {
		out.print("(bv-xor ");
		xor.left().accept(this);
		out.print(" ");
		xor.right().accept(this);
		out.print(")");
	}

	public void visit(ISHL shl) {
		if (!(shl.right() instanceof IntegerConstant)) {
			throw new RuntimeException("Can't handle ISHL with symbolic amount");
		}

		out.print("(bv-shift-left0 ");
		shl.left().accept(this);
		out.print(" ");
		out.print(shl.right());
		out.print(")");
	}

	public void visit(ISHR shr) {
		if (!(shr.right() instanceof IntegerConstant)) {
			throw new RuntimeException("Can't handle ISHR with symbolic amount");
		}

		out.print("(bv-shift-right0 ");
		shr.left().accept(this);
		out.print(" ");
		out.print(shr.right());
		out.print(")");
	}

	public void visit(IUSHR ushr) {
		if (!(ushr.right() instanceof IntegerConstant)) {
			throw new RuntimeException("Can't handle IUSHR with symbolic amount");
		}
		
		out.print("(let ((_x::(bitvector 32) ");
		ushr.left().accept(this);
		out.print(String.format(")) (ite (= (bv-extract 31 31 _x) (mk-bv 1 0))" + " (bv-shift-right0 _x %d)"
				+ " (bv-not (bv-shift-right0 (bv-not _x) %d)))" + ")", ushr.right(), ushr.right()));
	}

	public void visit(INEG neg) {
		out.print("(bv-neg ");
		neg.expression().accept(this);
		out.print(")");
	}

	public void visit(LADD add) {
		out.print("(bv-add ");
		add.left().accept(this);
		out.print(" ");
		add.right().accept(this);
		out.print(")");
	}

	public void visit(LSUB sub) {
		out.print("(bv-sub ");
		sub.left().accept(this);
		out.print(" ");
		sub.right().accept(this);
		out.print(")");
	}

	public void visit(LMUL mul) {
		out.print("(bv-mul ");
		mul.left().accept(this);
		out.print(" ");
		mul.right().accept(this);
		out.print(")");
	}

	public void visit(LDIV div) {
		out.print("(bv-udiv ");
		div.left().accept(this);
		out.print(" ");
		div.right().accept(this);
		out.print(")");
	}

	public void visit(LREM rem) {
		out.print("(bv-urem ");
		rem.left().accept(this);
		out.print(" ");
		rem.right().accept(this);
		out.print(")");
	}

	public void visit(LAND and) {
		out.print("(bv-and ");
		and.left().accept(this);
		out.print(" ");
		and.right().accept(this);
		out.print(")");
	}

	public void visit(LOR or) {
		out.print("(bv-or ");
		or.left().accept(this);
		out.print(" ");
		or.right().accept(this);
		out.print(")");
	}

	public void visit(LXOR xor) {
		out.print("(bv-xor ");
		xor.left().accept(this);
		out.print(" ");
		xor.right().accept(this);
		out.print(")");
	}

	public void visit(LSHL shl) {
		if (!(shl.right() instanceof IntegerConstant)) {
			throw new RuntimeException("Can't handle ISHL with symbolic amount");
		}

		out.print("(bv-shift-left0 ");
		shl.left().accept(this);
		out.print(" ");
		out.print(shl.right());
		out.print(")");
	}

	public void visit(LSHR shr) {
		if (!(shr.right() instanceof IntegerConstant)) {
			throw new RuntimeException("Can't handle ISHR with symbolic amount");
		}

		out.print("(bv-shift-right0 ");
		shr.left().accept(this);
		out.print(" ");
		out.print(shr.right());
		out.print(")");
	}

	public void visit(LUSHR ushr) {
		if (!(ushr.right() instanceof IntegerConstant)) {
			throw new RuntimeException("Can't handle IUSHR with symbolic amount");
		}

		out.print("(let ((_x::(bitvector 64) ");
		ushr.left().accept(this);
		out.print(String.format(")) (ite (= (bv-extract 63 63 _x) (mk-bv 1 0))" + " (bv-shift-right0 _x %d)"
				+ " (bv-not (bv-shift-right0 (bv-not _x) %d)))" + ")", ushr.right(), ushr.right()));
	}

	public void visit(LCMP cmp) {
		out.print("(let (");
		out.print("(_x::(bitvector 64) ");
		cmp.left().accept(this);
		out.print(") ");
		out.print("(_y::(bitvector 64) ");
		cmp.right().accept(this);
		out.print(")");
		out.print(") ");
		out.print("(ite (bv-sgt _x _y) (mk-bv 32 1) (ite (= _x _y) (mk-bv 32 1) 0b11111111111111111111111111111111))");
		out.print(")");
	}

	public void visit(LNEG neg) {
		out.print("(bv-neg ");
		neg.expression().accept(this);
		out.print(")");
	}

	public void visit(I2B i2b) {
		out.print("(bv-sign-extend (bv-extract 7 0 ");
		i2b.expression().accept(this);
		out.print(") 24)");
	}

	public void visit(I2L i2l) {
		out.print("(bv-sign-extend ");
		i2l.expression().accept(this);
		out.print(" 32)");
	}

	public void visit(I2C i2c) {
		out.print("(bv-sign-extend (bv-extract 15 0 ");
		i2c.expression().accept(this);
		out.print(") 16)");
	}

	public void visit(L2I l2i) {
		out.print("(bv-extract 31 0 ");
		l2i.expression().accept(this);
		out.print(")");
	}

	public void visit(EQ eq) {
		out.print("(= ");
		eq.left().accept(this);
		out.print(" ");
		eq.right().accept(this);
		out.print(")");
	}

	public void visit(GE ge) {
		out.print("(bv-sge ");
		ge.left().accept(this);
		out.print(" ");
		ge.right().accept(this);
		out.print(")");
	}

	public void visit(GT gt) {
		out.print("(bv-sgt ");
		gt.left().accept(this);
		out.print(" ");
		gt.right().accept(this);
		out.print(")");
	}

	public void visit(LE le) {
		out.print("(bv-sle ");
		le.left().accept(this);
		out.print(" ");
		le.right().accept(this);
		out.print(")");
	}

	public void visit(LT lt) {
		out.print("(bv-slt ");
		lt.left().accept(this);
		out.print(" ");
		lt.right().accept(this);
		out.print(")");
	}

	public void visit(NE ne) {
		out.print("(/= ");
		ne.left().accept(this);
		out.print(" ");
		ne.right().accept(this);
		out.print(")");
	}

	public void visit(NOT not) {
		out.print("(not ");
		not.constraint().accept(this);
		out.print(")");
	}

	public void visit(AND and) {
		out.print("(and");
		for(Constraint c: and.constraints()) {
			out.print(" ");
			c.accept(this);
		}
		out.print(")");
	}

	public void visit(OR or) {
		out.print("(or");
		for (Constraint c : or.constraints()) {
			out.print(" ");
			c.accept(this);
		}
		out.print(")");
	}
}
